Nuprl Lemma : scheme-constant_wf
11,40
postcript
pdf
R
:Realizer. scheme-constant(
R
)
RealizerScheme{i:l}()
latex
Definitions
Realizer
,
t
T
,
x
:
A
.
B
(
x
)
,
A
B
,
a
<
b
,
Void
,
x
:
A
B
(
x
)
,
P
Q
,
False
,
A
,
#$n
,
{
x
:
A
|
B
(
x
)}
,
,
,
Namer(
n
;
Id_list
)
,
Type
,
type
List
,
Id
,
x
:
A
B
(
x
)
,
x
.
A
(
x
)
,
[]
,
<
a
,
b
>
,
scheme-constant(
R
)
,
RealizerScheme{i:l}()
Lemmas
Id
wf
,
Namer
wf
,
le
wf
,
es
realizer
wf
origin
R:Realizer. scheme-constant(R) 
RealizerScheme{i:l}() R:Realizer. scheme-constant(R) RealizerScheme{i:l}() Tx:A. B(x)
B
B(x)
Q
A
B(x)
x.A(x)